/*
 * TreeToLPB.hpp
 *
 * Copyright 2012 Fabian Wenzelmann
 *
 * This file is part of Recognition-Procedures-for-Boolean-Functions.
 *
 * Recognition-Procedures-for-Boolean-Functions is free software: you
 * can redistribute it and/or modify it under the terms of the
 * GNU General Public License as published by the Free Software Foundation,
 * either version 3 of the License, or (at your option) any later version.
 *
 * Recognition-Procedures-for-Boolean-Functions is distributed in the hope
 * that it will be useful, but WITHOUT ANY WARRANTY; without even the implied
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General
 * Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with Recognition-Procedures-for-Boolean-Functions.
 *
 * If not, see <http://www.gnu.org/licenses/>.
 */

#ifndef TREETOLPB_HPP_
#define TREETOLPB_HPP_

#include <string>

#include "bfr/LPBConversionException.hpp"
#include "bfr/lpbCombinatorial/SplittingTree.hpp"
#include "bfr/lpbCombinatorial/SolverInformation.hpp"
#include "bfr/lpbCombinatorial/CoefficientSelectionException.hpp"
#include "bfr/LPB.hpp"

namespace bfr {

template<class ChooserT>
class TreeToLPB {
    public:
        explicit TreeToLPB(const ChooserT &c=ChooserT())
    : chooser(c), information() {
        }
        ~TreeToLPB() { }

        /**
         * Choose the degree in the interval \f$(a, b]\f$.
         *
         * Tries to choose the degree of the LPB in the interval
         * \f$(a, b]\f$. If this is not possible an exception is thrown.
         *
         * BIG TODO
         * We just test if there is an integer solution, but because a and
         * b are integers as well this should be ok.
         *
         * Can someone think about it? ;)
         *
         * @param a First value of the interval.
         * @param b Second value of the interval.
         */
        lpb_coefficient_t chooseDegree(lpb_coefficient_t a,
                lpb_coefficient_t b)
        const throw(LPBConversionException) {
            if ((a == coeff_pos_infinity) || (b == coeff_neg_infinity))
                throw LPBConversionException(errorMessage(a, b));
            else if (a == coeff_neg_infinity) {
                if (b == coeff_neg_infinity) {
                    throw LPBConversionException(errorMessage(a, b));
                }
                else if (b == coeff_pos_infinity) {
                    return 0;
                }
                else {
                    // b is a number
                    return b;
                }
            }
            else {
                // a is a number
                if (b == coeff_pos_infinity) {
                    return a + 1;
                }
                else {
                    // a and b are numbers
                    lpb_coefficient_t smallestSol = a + 1;
                    if (smallestSol > b) {
                        // TODO: what if we can choose the coefficient,
                        // but not as an integer?
                        if (a < b) {
                            std::cout << "BUG: See TreeToLPB chooseDegree."
                                    << "Degree just can't be an integer."
                                    << std::endl;
                        }
                        throw LPBConversionException(errorMessage(a, b));
                    }
                    else {
                        return smallestSol;
                    }
                }
            }
        }

        void flagRepair() {//do nothing
	}    
        bool getRepairFlag() {
	  return false;
	} 

        LPB *solve(SplittingTree *tree)
        throw(LPBConversionException) {
            // actually we do not start with column index tree.size() - 1
            // because then we must use while (k >= 0) what is not good
            // for size_t because it will always be >= 0
            size_t k = tree->size();
            const size_t numVariables = tree->size() - 1;
            information.init(*tree);
            while (k) {
                interval_t res = tree->handleColumn(k - 1, chooser, information);
                lpb_coefficient_t max = res.first;
                lpb_coefficient_t min = res.second;
                if ((max + 1) == min) {
                    // yes, we have a conflict
                    // use the information to solve the conflict
                    interval_t newValues =
                            information.solveConflict(k - 1, max, min);
                    max = newValues.first;
                    min = newValues.second;
                }
                try {
                    // different from java version, but should be correct
                    if (k != 1) {
                        // TODO k - 1 correct?
                        const lpb_coefficient_t coeff =
                                chooser.chooseCoefficient(max, min,
                                        tree->getContext(),
                                        information, k - 1);
                        information.setCoefficient(k - 1, coeff);
                    }
                } catch (const CoefficientSelectionException &e) {
                    throw LPBConversionException(e.what());
                }
                --k;
            }
            interval_t rootInterval =
                    information.getInterval(*(tree->getRoot()));
            lpb_coefficient_t degree =
                    chooseDegree(rootInterval.first, rootInterval.second);
            LPB *result = new LPB(degree, numVariables);
            VariableSetting *vs = tree->getVariableSetting();
            for (size_t i = 0; i < numVariables; i++) {
                size_t literalID = vs->operator[](i);
                result->addSummand(information.getCoefficient(i + 1),
                        Literal(literalID));
            }
            return result;
        }

    protected:
        /**
         * Construct an error message.
         *
         * The returned message says that it is not possible to
         * choose the degree in the interval (a, b].
         *
         * @param a First value of the interval.
         * @param b Second value of the interval.
         *
         * @return Error message.
         */
        inline std::string errorMessage(lpb_coefficient_t a,
                lpb_coefficient_t b) const {
            std::ostringstream error;
            error << "Can't choose degree in the interval (" <<
                    a << ", " << b << "].";
            return error.str();
        }

    private:
        ChooserT chooser;
        SolverInformation information;
};

}



#endif  // TREETOLPB_HPP_
